package mac5789.sat;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Random;
import java.util.Set;

/**
 * Implementação de problema aleatório, de acordo com alguns parâmetros.
 * Gera problemas com número definido de variáveis de cláusulas, usando sempre cláusulas 3-SAT.
 * @author lundberg
 *
 */
public class RandomSatProblem implements SatProblem {

	private static final int LITERALS_PER_CLAUSE = 3;

	private final int nVariables;

	private final int nClauses;

    private String format = "cnf";

	private List<Integer[]> generatedClauses = null;

	private Random random;
	
	private Set<Set<Integer>> clauses = new HashSet<Set<Integer>>();
	
	private Set<Integer> missingAtoms = new HashSet<Integer>();
	
	private List<Set<Integer>> clauseList = new ArrayList<Set<Integer>>();
	
	private Map<Integer, Integer> atomCount = new HashMap<Integer, Integer>();

	/**
	 * Construtor
	 * @param seed semente do gerador de números pseudo-aleatórios
	 * @param nVariables número de variáveis desejado
	 * @param nClauses número de cláusulas que o problema deve ter
	 */
	public RandomSatProblem(long seed, int nVariables, int nClauses) {
		super();
		this.nVariables = nVariables;
		this.nClauses = nClauses;
		this.random = new Random(seed);
	}

	@Override
	public String getFormat() {
        return this.format;
	}

	@Override
	public int getNVariables() {
		return nVariables;
	}

	@Override
	public int getNClauses() {
		return nClauses;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public Iterator<Integer[]> iterator() {
		return this.getClauses();
	}

	/**
	 * Gera cláusulas pseudo-aleatórias.
	 */
	@Override
	public Iterator<Integer[]> getClauses() {
		if(generatedClauses == null) {
			initializeAtomCount();
			expandFormula();
			replaceUntilAllVariablesUsed();
			storeClauseList(clauses);
		}
		return generatedClauses.iterator();
	}

	/**
	 * Inicializa a contagem de literais
	 * @param atomCount atomCount
	 */
	private void initializeAtomCount() {
		for(int atom = 1; atom <= nVariables; atom++) {
			atomCount.put(atom, 0);
			missingAtoms.add(atom);
		}
	}

	/**
	 * Expande a fórmula, gerando e adicionando novas cálsulas até que o número de cláusulas seja atingido.
	 */
	private void expandFormula() {
		while(clauses.size() < nClauses) {
			add(generateClause());
		}
	}

	/**
	 * Enquanto existem variáveis não utilizadas, gera novas cláusulas não presentes na fórmula e substitui
	 * fórmulas escolhidas pseudoaleatoriamente da fórmula.
	 * Ao fim, existe o número de cláusulas desejado e o número de variáveis.
	 */
	private void replaceUntilAllVariablesUsed() {
		while(!missingAtoms.isEmpty()) {
			Set<Integer> candidate = generateClause(missingAtoms.iterator().next());
			if(!clauses.contains(candidate)) {
				Set<Integer> toRemove = clauseList.get(random.nextInt(nClauses));
				remove(toRemove);
				add(candidate);
			}
		}
	}

	/**
	 * Cria uma cláusula pseudoaleatória
	 * @param random random
	 * @return conjunto de literais que compoe uma cláusula
	 */
	private Set<Integer> generateClause(Integer... forcedAtoms) {
		Set<Integer> atoms = new HashSet<Integer>(Arrays.asList(forcedAtoms));
		while(atoms.size() < LITERALS_PER_CLAUSE) {
			Integer atom = random.nextInt(nVariables) + 1;
			atoms.add(atom);
		}
		Set<Integer> clause = new HashSet<Integer>();
		for(Integer atom : atoms) {
			boolean negate = random.nextBoolean();
			clause.add(negate ? -atom : atom);
		}
		return clause;
	}

	/**
	 * Adiciona uma cláusula à fórmula, atualizando as estruturas de dados de controle.
	 * @param clauses clauses
	 * @param clauseList clauseList
	 * @param atomCount atomCount
	 * @param candidate candidate
	 */
	private void add(Set<Integer> candidate) {
		if(clauses.add(candidate)) {
			clauseList.add(candidate);
			for(Integer literal : candidate) {
				Integer atom = Math.abs(literal);
				Integer count = atomCount.get(atom);
				atomCount.put(atom, count + 1);
				if(count == 0) {
					missingAtoms.remove(atom);
				}
			}
		}
	}

	/**
	 * Remove a cláusula da fórmula, atualizando as estrutudas de dados de controle.
	 * @param clauses clauses
	 * @param clauseList clauseList
	 * @param atomCount atomCount
	 * @param removed removed
	 */
	private void remove(Set<Integer> removed) {
		clauses.remove(removed);
		clauseList.remove(removed);
		for(Integer literal : removed) {
			Integer atom = Math.abs(literal);
			Integer count = atomCount.get(atom);
			atomCount.put(atom, atomCount.get(atom) - 1);
			if(count == 1) {
				missingAtoms.add(atom);
			}
		}
	}

	/**
	 * Parte de um conjunto de conjuntos de literais e contrói um iterador de array de inteiros, adequado à interface do problema.
	 * @param clauses clauses
	 * @return Iterator
	 */
	private void storeClauseList(Set<Set<Integer>> clauses) {
		generatedClauses = new ArrayList<Integer[]>(nClauses);
		for(Set<Integer> clause : clauses) {
			generatedClauses.add(clause.toArray(new Integer[clause.size()]));
		}
	}
}
